Nuprl Lemma : atom-free-ecl-trans-type 0,22

ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da).
AtomFree(Type;ecl-trans-type(ecl-trans(x))) 
latex


Definitions, Type, #$n, , s = t, t  T, Unit, left+right, AtomFree(T;x), ecl-trans-type(A), ecl-base-tuple(k;test), x:AB(x), P  Q, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-add-catch(A;l), x:AB(x), ecl-trans-tuple{i:l}(ds;da), ecl-trans(x), x:AB(x), ecl-add-throw(A;m), add-ecl-act(A;m), reset-ecl-tuple(A), State(ds), Valtype(da;k), x.A(x), combine-ecl-tuples2(A;B;f;g), combine-ecl-tuples(A;B;f;g), ecl ind eclcatch compseq tag def, ecl ind eclthrow compseq tag def, ecl ind eclact compseq tag def, ecl ind eclrepeat compseq tag def, ecl ind eclor compseq tag def, ecl ind ecland compseq tag def, ecl ind eclseq compseq tag def, ecl ind eclbase compseq tag def, ecl(ds;da), , type List, False, A, AB, {x:AB(x) }, Knd, {T}, xt(x), Id, a:A fp B(a)
Lemmasfpf wf, Id wf, ecl-induction, Knd wf, ecl-trans-type wf, nat wf, ecl wf, unit wf, ma-valtype wf, decl-state wf, ecl-trans wf, ecl-trans-tuple wf, atom-free wf, bool wf

origin